a, b:. a < b  a  b 

latex

Definitions	x,y. t(x;y), , x f y, t  T, OMon, t.1, Mon, x(s1,s2), P & Q, AbMon, OCMon, OGrp, <+>, |g|, x:A. B(x), r  s, r < s
Lemmas	ocgrp wf, grp le wf, assert wf, grp car wf, linorder wf, qadd grp wf2, grp leq weakening lt